--- Recreate a type with type aliases from a 'Tau' type.

module frege.compiler.common.UnAlias where 

import  frege.Prelude  hiding(error, print, println, break, <+>)
import  frege.data.TreeMap as TM(TreeMap, lookup, each, insert, union, including, contains, keys, values, fromKeys)
import  frege.compiler.enums.Flags
import  frege.compiler.types.Positions
import  frege.compiler.types.Types
import  frege.compiler.types.Symbols
import  frege.compiler.types.Global  as  G
import  frege.compiler.classes.QNameMatcher(QNameMatcher)

{--
    'unAlias' tries to replace a TApp with an application of 
    some type alias that would give the same type back.
    
    Note that 'unAlias' returns a pseudo type that is *no good for anything* except printing!
    
    'unAlias' works only on _type applications_. 
    This is because it is clearly not desirable to unalias simple types
    like 'Int' in the presence of 
    
    > type Money = Int
    > type Age   = Int
    
    There is no way to say whether the 'Int' in question was 'Money',
    'Age' or just 'Int' in the original, 
    and hence unaliasing every 'Int' to 'Money', say,
    would produce confusing types.
    -}
-- unAlias :: QNameMatcher a => Global -> TauT a -> Tau
unAlias g tau 
        = if isOn g.options.flags SPECIAL then fake g tau else unAlias (fake g tau)
    where
        -- make sure we work on a 'TauT' 'QName'
        fake ∷ QNameMatcher a => Global → TauT a → Tau
        fake g (TApp a b)           = TApp (fake g a) (fake g b)
        fake g TVar{pos,var,kind}   = TVar Position.null (kmap g kind) var
        fake g (Meta Rigid{hint, kind})   = TVar Position.null (kmap g kind) hint
        fake g (Meta x)        = case g.bound  x of
            Just tau      -> tau
            otherwise     -> TVar Position.null (kmap g x.kind) ("t" ++ show x.uid)
        fake g TCon{pos, name}  = TCon{pos, name = fakeQName name}
        fake g (TSig s)        = TSig (fakeSigma g s)

        kmap ∷ QNameMatcher a => Global -> KindT a → Kind
        kmap g (KGen t)     = KGen (map (fake g) t)
        kmap g KType        = KType
        kmap g (KApp a b)   = KApp (kmap g a) (kmap g b)
        kmap g KVar         = KVar

        fakeSigma ∷ QNameMatcher a => Global -> SigmaT a → Sigma
        fakeSigma g (ForAll{bound, rho}) = ForAll (map (fake g) bound) (fakeRho g rho)
        fakeRho ∷ QNameMatcher a => Global -> RhoT a → Rho
        fakeRho g (r@RhoFun{context, sigma, rho}) 
            = RhoFun{context = map (fakeCtx g) r.context, 
                     sigma   = fakeSigma g r.sigma, 
                     rho     = fakeRho g r.rho}
        fakeRho g (r@RhoTau{context, tau}) 
            = RhoTau{context = map (fakeCtx g) context, tau = fake g tau}
        fakeCtx ∷ QNameMatcher a => Global -> ContextT a → Context
        fakeCtx g ctx = Ctx{tau = fake g ctx.tau, cname = fakeQName ctx.cname, pos = ctx.pos}  

        unAlias ∷ Tau → Tau
        unAlias  tau = case tau of
                -- TFun a b       -> TFun (unAlias a) (unAlias b)
                TApp a b       -> case mapMaybe (aliased tau) aliases of
                                        []      -> TApp (unAlias a) (unAlias b)
                                        (ali:_) -> ali
                _              -> tau
            where

                aliased (tau1@TApp a b) (SymA{pos,name,typ,vars}) = case rho of
                        -- the expansion of the type alias must be more than a tvar 
                        RhoTau [] tau2 | not (isTvApp tau2) -> case unify empty tau2 tau1 of
                            Just subst -> Just (substTau env aApp)
                                where env = fmap unAlias subst
                            Nothing    -> Nothing
                        _              -> Nothing
                    where
                        rho = typ.rho
                        vs  = map Tau.var vars
                        aApp :: Tau
                        aApp = fold TApp (TCon pos name) (map (TVar pos KVar) vs)

                aliased _ _ = Nothing

                aliases = [ sym | any <- values g.thisTab, sym@SymA{} <- g.follow any ]


                -- substTau env (TFun a b)  = TFun (substTau env a) (substTau env b)
                substTau :: TreeMap String (TauT β) -> TauT β -> TauT β
                substTau env (TApp a b)  = TApp (substTau env a) (substTau env b)
                substTau env (TVar{var})
                    | Just tau <- lookup var env  = tau
                substTau env tau         = tau


                -- unify t (TFun a b) (TFun c d) = do
                --         t1 <- unify t  a c
                --         t2 <- unify t1 b d
                --         return t2
                unify t (Meta x) (Meta y) | x.uid == y.uid = Just t
                unify t TCon{name=name1} TCon{name=name2} |  match g name1 name2 = Just t
                unify t (TApp a b) (TApp c d) = do
                        t1 <- unify t  a c
                        t2 <- unify t1 b d
                        return t2
                unify t TVar{var} tau = case lookup var t of
                        Nothing  -> Just (insert var tau t)         -- extend substitution
                        Just old -> case unify empty old tau of       -- check if previous substitution matches current
                            Just sub | all varSelf (each sub) = Just t
                            _                                 = Nothing
                    where
                        -- checks whether each variable would be substituted by itself
                        -- if all substitutions are of this form, then we have type equality
                        varSelf (s, TVar{var}) = s == var
                        varSelf _              = false
                unify t _ _ = Nothing


